﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System.Collections.Generic;
using System;
using Core;

namespace Formality.FormalSystem.Reasoning
{
    public class Substitution : Tuple<Function, Proposition>
    {
        public Substitution(Function Func, Proposition Prop)
            : base(Func, Prop)
        {
        }

        public Function Func
        {
            get { return Item1; }
        }

        public Proposition Prop
        {
            get { return Item2; }
        }

        public Proposition Expand(Function From)
        {
            var VarMap = new VariableRenaming.Search(Func.Proposition, From.Proposition).Perform();

            return VarMap != null ? Expand(Prop, VarMap) : null;
        }

        private static Proposition Expand(Proposition Prop, VariableRenaming.Justification VarMap)
        {
            Func<Proposition, Proposition> Self = p => Expand(p, VarMap);

            return new Proposition(Prop, VarMap.ApplyMap, Self);
        }
    }

    public class SubstitutionMap
    {
        private readonly Dictionary<Variable, Substitution> Map;

        public SubstitutionMap()
        {
            Map = new Dictionary<Variable, Substitution>();
        }

        public SubstitutionMap(SubstitutionMap Basis)
        {
            Map = new Dictionary<Variable, Substitution>(Basis.Map);
        }

        public Substitution this[Variable v]
        {
            get { return Map[v]; }
            set { Map[v] = value; }
        }

        public Proposition ApplySubstitutions(Proposition Prop)
        {
            if (Prop.Type != PropType.Function)
                return new Proposition(Prop, v => v, ApplySubstitutions);

            var f = new Function(Prop);

            Substitution Sub;

            return TryGetValue(f.Name, out Sub) ? Sub.Expand(f) : Prop;
        }

        public bool TryGetValue(Variable v, out Substitution Sub)
        {
            return Map.TryGetValue(v, out Sub);
        }

        public bool HasSubstitution(Variable v)
        {
            return Map.ContainsKey(v);
        }


    }
}